at src(l):
action $a(m) 
precondition P
psends [$tg,f] on link l
== ([@source(l) precondition for "$a"(v:A):
== ([@source(l) P State(ds) v
== (; sends locl("$a")(v:A) on l:
== (; tagged([<"$tg",s,v. [f(s,v)]>],State(ds),v):"$tg" : T
== (; only events in [locl("$a")] send on l with "$tg"]) 

latex

---

clarification:

weakPrecondSendR{$a,$tg}(T;A;l;ds;P;f)
== ([@source(l) precondition for "$a"(v:A):
== ([@source(l) P State(ds) v
== (; sends locl("$a")(v:A) on l:
== (; tagged(<"$tg",s,v. (f(s,v)).nil>.nil,State(ds),v):"$tg" : T
== (/ only events in locl("$a").nil send on l with "$tg".nil]) 

latex

Definitions	(L), @loc precondition for a(v:T):P State(ds) v, source(l), sends knd(v:T) on l:tagged(g,State(ds),v):dt, x : v, <a,b>, x.A(x), f(a), only events in L send on lnk with tag, car.cdr, locl(a), "$x", nil
FDL editor aliases	weakPrecondSendR